Bob is not cold. Bob is round. Charlie is green. Charlie is young. Erin is white. Harry is green. Harry is young. White things are round. If something is green and not young then it is round. If something is young then it is white. If something is cold then it is big. If something is young and not cold then it is big. Round, young things are smart.
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is round.
("Bob" "is" "round" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is young.
("Harry" "is" "young" "+")
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is green and not young then it is round.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
If something is young then it is white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is young and not cold then it is big.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "big" "+"))
Round, young things are smart.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Harry is green.
True
1
proof
[(triple6)]
("Harry" "is" "green" "+")
triple6
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Erin is round.
True
2
proof
[(((triple5) -> rule1))]
("Erin" "is" "round" "+")
((triple5) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "white" "-")
((triple7) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
True
3
proof
[(((((triple7) -> rule3)) -> rule1))]
("Harry" "is" "round" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Charlie is not round.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("Charlie" "is" "round" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
True
5
proof
[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule6))]
("Charlie" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Harry is not smart.
False
5
inv-proof
[(((((((triple7) -> rule3)) -> rule1) triple7) -> rule6))]
("Harry" "is" "smart" "-")
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "smart" "+")
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "big" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "big" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Bob is not cold.[(triple1)] Bob is round.[(triple2)] Charlie is green.[(triple3)] Charlie is young.[(triple4)] Erin is white.[(triple5)] Harry is green.[(triple6)] Harry is young.[(triple7)] @1: Charlie is white.[(((triple4) -> rule3))] Erin is round.[(((triple5) -> rule1))] Harry is white.[(((triple7) -> rule3))] @2: Charlie is round.[(((((triple4) -> rule3)) -> rule1))] Harry is round.[(((((triple7) -> rule3)) -> rule1))] @3: Charlie is smart.[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule6))] Harry is smart.[(((((((triple7) -> rule3)) -> rule1) triple7) -> rule6))]
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
((triple4) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple5) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3