Dave is blue. Dave is cold. Dave is round. Dave is not white. Dave is young. Fiona is cold. Fiona is smart. Fiona is young. Harry is blue. Harry is cold. Harry is green. Harry is round. Harry is smart. Harry is white. Harry is young. White things are cold. If something is round and cold then it is young. If something is blue and not round then it is white. If Dave is blue and Dave is white then Dave is smart. If something is young then it is green. If something is young and not cold then it is not green.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not white.
("Dave" "is" "white" "-")
Dave is young.
("Dave" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is round and cold then it is young.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is blue and not round then it is white.
((("something" "is" "blue" "+") ("something" "is" "round" "~")) -> ("something" "is" "white" "+"))
If Dave is blue and Dave is white then Dave is smart.
((("Dave" "is" "blue" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "smart" "+"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is young and not cold then it is not green.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "green" "-"))
Fiona is smart.
True
1
proof
[(triple7)]
("Fiona" "is" "smart" "+")
triple7
Harry is not green.
False
1
inv-proof
[(triple11 OR ((triple15) -> rule5) OR ((((triple12 triple10) -> rule2)) -> rule5) OR ((((triple12 ((triple14) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "green" "-")
triple11
((triple15) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple12 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple12 ((triple14) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Fiona is green.
True
2
proof
[(((triple8) -> rule5))]
("Fiona" "is" "green" "+")
((triple8) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple8) -> rule5))]
("Fiona" "is" "green" "-")
((triple8) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "smart" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Dave is not white.[(triple4)] Dave is round.[(triple3)] Dave is young.[(triple5 OR ((triple3 triple2) -> rule2))] Fiona is cold.[(triple6)] Fiona is smart.[(triple7)] Fiona is young.[(triple8)] Harry is blue.[(triple9)] Harry is cold.[(triple10 OR ((triple14) -> rule1))] Harry is green.[(triple11 OR ((triple15) -> rule5) OR ((((triple12 triple10) -> rule2)) -> rule5) OR ((((triple12 ((triple14) -> rule1)) -> rule2)) -> rule5))] Harry is round.[(triple12)] Harry is smart.[(triple13)] Harry is white.[(triple14)] Harry is young.[(triple15 OR ((triple12 triple10) -> rule2) OR ((triple12 ((triple14) -> rule1)) -> rule2))] @1: Dave is green.[(((triple5) -> rule5) OR ((((triple3 triple2) -> rule2)) -> rule5))] Fiona is green.[(((triple8) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is not white.
("Dave" "is" "white" "-")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple5
((triple3 triple2) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Fiona is young.
("Fiona" "is" "young" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
((triple14) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple11
((triple15) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple12 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple12 ((triple14) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
((triple12 triple10) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple12 ((triple14) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple5) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple3 triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((triple8) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1