Bob is green. Bob is red. Charlie is round. Dave is green. Fiona is not nice. Fiona is round. Fiona is young. White things are not nice. If something is young and red then it is not nice. If something is green then it is young. All white, smart things are young. Red, smart things are not young. All red, round things are not white. All green things are not smart. If something is young and red then it is round.
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is green.
("Dave" "is" "green" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
White things are not nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "-"))
If something is young and red then it is not nice.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
If something is green then it is young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All white, smart things are young.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Red, smart things are not young.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "-"))
All red, round things are not white.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
All green things are not smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
If something is young and red then it is round.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Fiona is round.
True
1
proof
[(triple6)]
("Fiona" "is" "round" "+")
triple6
Fiona is not young.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "young" "-")
triple7
Bob is not smart.
True
2
proof
[(((triple1) -> rule7))]
("Bob" "is" "smart" "-")
((triple1) -> (rule7 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Dave is smart.
False
2
inv-proof
[(((triple4) -> rule7))]
("Dave" "is" "smart" "+")
((triple4) -> (rule7 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Bob is round.
True
4
proof
[(((((triple1) -> rule3) triple2) -> rule8))]
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not round.
False
4
inv-proof
[(((((triple1) -> rule3) triple2) -> rule8))]
("Bob" "is" "round" "-")
((((triple1) -> (rule3 % int2)) triple2) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not white.
True
6
proof
[(((triple2 ((((triple1) -> rule3) triple2) -> rule8)) -> rule6))]
("Bob" "is" "white" "-")
((triple2 ((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
False
6
inv-proof
[(((triple2 ((((triple1) -> rule3) triple2) -> rule8)) -> rule6))]
("Bob" "is" "white" "+")
((triple2 ((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "round" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is green.[(triple1)] Bob is red.[(triple2)] Charlie is round.[(triple3)] Dave is green.[(triple4)] Fiona is not nice.[(triple5)] Fiona is round.[(triple6)] Fiona is young.[(triple7)] @1: Bob is not smart.[(((triple1) -> rule7))] Bob is young.[(((triple1) -> rule3))] Dave is not smart.[(((triple4) -> rule7))] Dave is young.[(((triple4) -> rule3))] @2: Bob is not nice.[(((((triple1) -> rule3) triple2) -> rule2))] Bob is round.[(((((triple1) -> rule3) triple2) -> rule8))] @3: Bob is not white.[(((triple2 ((((triple1) -> rule3) triple2) -> rule8)) -> rule6))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple5
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Bob is not smart.
("Bob" "is" "smart" "-")
((triple1) -> (rule7 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is not smart.
("Dave" "is" "smart" "-")
((triple4) -> (rule7 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
((triple2 ((((triple1) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3