Bob is kind. Charlie is nice. Fiona is rough. Harry is kind. Kind people are white. If someone is white and kind then they are big. If someone is big then they are white. Rough people are round. If someone is big then they are red. White, kind people are big.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is white and kind then they are big.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
White, kind people are big.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Fiona is rough.
True
1
proof
[(triple3)]
("Fiona" "is" "rough" "+")
triple3
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Harry is white.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "white" "+")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "-")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule2) OR ((((triple1) -> rule1) triple1) -> rule6))]
("Bob" "is" "big" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not big.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule2) OR ((((triple1) -> rule1) triple1) -> rule6))]
("Bob" "is" "big" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Harry is red.
True
5
proof
[(((((((triple4) -> rule1) triple4) -> rule2)) -> rule5) OR ((((((triple4) -> rule1) triple4) -> rule6)) -> rule5))]
("Harry" "is" "red" "+")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not red.
False
5
inv-proof
[(((((((triple4) -> rule1) triple4) -> rule2)) -> rule5) OR ((((((triple4) -> rule1) triple4) -> rule6)) -> rule5))]
("Harry" "is" "red" "-")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Fiona is not white.
Unknown
inv-rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Fiona" "is" "red" "+")
Charlie is not white.
Unknown
inv-rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "white" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "round" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Bob is kind.[(triple1)] Charlie is nice.[(triple2)] Fiona is rough.[(triple3)] Harry is kind.[(triple4)] @1: Bob is white.[(((triple1) -> rule1))] Fiona is round.[(((triple3) -> rule4))] Harry is white.[(((triple4) -> rule1))] @2: Bob is big.[(((((triple1) -> rule1) triple1) -> rule2) OR ((((triple1) -> rule1) triple1) -> rule6))] Harry is big.[(((((triple4) -> rule1) triple4) -> rule2) OR ((((triple4) -> rule1) triple4) -> rule6))] @3: Bob is red.[(((((((triple1) -> rule1) triple1) -> rule2)) -> rule5) OR ((((((triple1) -> rule1) triple1) -> rule6)) -> rule5))] Harry is red.[(((((((triple4) -> rule1) triple4) -> rule2)) -> rule5) OR ((((((triple4) -> rule1) triple4) -> rule6)) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((((triple1) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3